\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$, ${\it e'}$:E.
\\[0ex]f2f+{-}pred($e$,${\it e'}$)
\\[0ex]$\Rightarrow$ \=(([$e$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\Rightarrow$ [${\it e'}$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])\+
\\[0ex]\& ([$e$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$] $\Rightarrow$ [${\it e'}$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$]))
\-
\end{tabbing}